D:Dsys, sched:(Id((IdLnk+Id)+Unit)), v:(i:IdM(i).state),
dec:(i,a:IdM(i).state(M(i).da(locl(a))+Unit)), t:.
Feasible(D)  d-comp-partial-world(D;v;sched;dec;t)  World 

latex

Definitions

Dsys, t  T, Unit, Type, Id, IdLnk, left+right, , x:AB(x), x:A. B(x), M(i), M.state, locl(a), M.da(a), Feasible(D), d-comp-partial-world(D;v;sched;dec;t), World, P  Q, False, A, AB, , {x:A| B(x) }, d-comp(D;v;sched;dec), d-world-state(D;i), #$n, {i..j}, s = t, d-partial-world(D;f;t';s), x.A(x), Prop, b, b, , i=j, x:AB(x), P & Q, P  Q, f(a), M.init(x)?v, State(ds), 1of(t), -n, n+m, a<b, Void, n-m, CV(F), S  T, i  j < k, S  T

Lemmas

CV wf, le wf, ma-init-val wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bool wf, bnot wf, not wf, assert wf, d-partial-world wf, int seg wf, d-world-state wf, d-comp wf2, d-feasible wf, ma-da wf, locl wf, ma-st wf, d-m wf, nat wf, IdLnk wf, Id wf, unit wf, dsys wf